%\documentclass{article}
%\documentclass[11pt]{article}

\documentclass[prodmode,acmtist]{acmsmall}

% Package to generate and customize Algorithm as per ACM style
\usepackage[ruled]{algorithm2e}
\renewcommand{\algorithmcfname}{ALGORITHM}
\SetAlFnt{\small}
\SetAlCapFnt{\small}
\SetAlCapNameFnt{\small}
\SetAlCapHSkip{0pt}
\IncMargin{-\parindent}

%\documentclass[preprint]{elsarticle}
%\documentclass[final,1p,times]{elsarticle}

\usepackage{epsfig}
\usepackage{subfigure,fancyvrb}
\usepackage{amsfonts}
\usepackage{times}
\usepackage{helvet}
\usepackage{courier}
\usepackage{graphics}
\usepackage{colordvi,epsfig,multirow,amsmath,amssymb}


\setlength{\voffset}{-0.4in}
\def\qed{\hspace*{\fill} $\blacksquare$}
\newcommand{\nop}[1]{}

%\newtheorem{defn}{Definition}
\newtheorem{thm}{Theorem}
\nop{
%for AIJ 
\newtheorem{thm}{Theorem}
%\newtheorem{thmrem}{Theorem}
\newtheorem{lemma}[thm]{Lemma}
%\newtheorem{lemrmk}[thmrem]{Lemma}
\newtheorem{ex}{Example}

\newdefinition{defn}{Definition}
\newproof{proof}{Proof}
%\newproof{pot}{Proof of Theorem \ref{thm2}}
}

%\newtheorem{proof}{Proof}


%\pagestyle{plain}
%\bibliographystyle{plain}

%\newcommand{\BibTeX}{{\rm B\kern-.05em{\sc i\kern-.025em b}\kern-.08em T\kern-.1667em\lower.7ex\hbox{E}\kern-.125emX}}

%\newcommand{\goodgap}{%  \hspace{\subfigcapskip}}


%\newenvironment{proof}{\noindent {\bf Proof} \,}{$\: \sqcap \! \! \! \!
%  \sqcup $ \\}
\nop{
\newtheorem{theorem}{Theorem}[section]
\newtheorem{subtheorem}{Theorem}[subsection]
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newdef{defn}[theorem]{Definition}
\newdef{remark}[theorem]{Remark}
}
\newdef{defn}[theorem]{Definition}
%\renewcommand{\arraystretch}{1.0}
%\nop{ \acmVolume{} \acmNumber{} \acmYear{} \acmMonth{} }
\markboth{Ruoyun Huang et al}{A SAT-based Solver for Cost Sensitive Temporally Expressive Planning}





\title{A SAT-based Solver for Cost Sensitive Temporally Expressive Planning}
%\tnotetext[t2]{This research was supported by China Scholarship
%Council, NSF grants IIS-0535257, DBI-0743797, IIS-0713109, and
%Microsoft Research New Faculty Fellowship.}

\author{RUOYUN HUANG$^{1,\dag}$, QIANG LU$^{2,\dag}$, YIXIN CHEN$^{1,\S}$, YOU XU$^1$, WEIXIONG ZHANG$^1$, and GUOLIANG CHEN$^2$\\
$^1$Washington University in St. Louis,
$^2$University of Science and Technology of China
%\{rh11,chen,yx2,zhang\}@cs.wustl.edu
}

%\date{}



\begin{abstract}
Complex features, such as temporal dependencies and numerical cost constraints, are hallmarks of real-world planning problems.
%Many real-world planning problems require a proper handling of
%complex features such as temporal expressiveness and numerical costs. 
In this paper, we consider the challenging problem of
cost-sensitive temporally expressive (CSTE) planning, which requires
concurrency of durative actions and optimization of action costs.
%CSTE is a difficult but important problem with many potential applications. 
%Particularly, we develop the first CSTE planning algorithm. 
%R.Huang I deleted the 'first' thing
We first propose a scheme to translate a CSTE planning
problem to a minimum cost (MinCost) satisfiability (SAT) problem,
which is an optimization problem with constraints represented in
SAT. We then develop a MinCost SAT solver to find solution plans
that optimize temporal makespan and minimize total action costs.
%multiple metrics, 
%an objective function that takes multiple cost metrics into account, 
%including temporal makespan and total action costs. 
We propose an approach to solving MinCost SAT, 
%The first is based on a transformation of a MinCost SAT problem
%to a weighted partial Max-SAT, and the second, 
called BB-DPLL, which is an
integration of the branch-and-bound technique and the DPLL method.
There are two critical components of BB-DPLL: a scheme for estimating
the lower bound of plan cost and a scheme for variable branching. 
Both techniques significantly improve the search efficiency. 
Our contribution is a temporally expressive planner that can optimize makespan and further minimize total action costs at the optimal makespan.
Our experiments on existing CSTE benchmark domains show that our planner
compares favorably to existing temporally expressive planners in terms of both efficiency and quality.
%Moreover, our
%planner is the only temporally expressive planner that can optimize
%action costs.
\end{abstract}

\category{I.2.8}{ARTIFICIAL INTELLIGENCE}{Problem Solving, Control Methods, and Search}[Plan execution, formation, and generation]
\terms{Algorithms}
\keywords{Planning; Temporal dependency; Numerical cost constraint; Satisfiability}

\begin{document}


\begin{bottomstuff}
$^\dag$Joint first authors with equal contribution.\\
$^\S$Corresponding author: Department of
Computer Science and Engineering, Washington University in St.
Louis, Saint Louis, MO 63130, USA. 
%Phone: +1 (314) 935-7528. 
E-mail: chen@cse.wustl.edu.  
\end{bottomstuff}

\maketitle

\setcounter{page}{1}


%%%%%%%%%%  Main Part *****************
\input{1.intro}
\input{2.background}


\input{3.encoding}
%\input{4.max-sat}
\input{5.opt}
%\input{6.peer}
%\input{6.concurrency}

\input{7.experiments}
\input{8.relatedwork}
\input{9.conclusion}

\begin{acks}
%\section{Acknowledgments}
\normalsize

This research was supported by China Scholarship
Council, NSF grants IIS-0535257, DBI-0743797, IIS-0713109, CNS 1017701, and
Microsoft Research New Faculty Fellowship.
%We thank Miguel Ram\'irez for the suggestion of applying Max-SAT solvers to MinCost SAT problems.

\end{acks}

\normalsize

%\bibliographystyle{natbib}
\bibliographystyle{acmsmall}
\bibliography{huang,lu}

\elecappendix

\medskip


% add "Appendix" to the section heading
\newcommand{\appsection}[1]{\let\oldthesection\thesection
  \renewcommand{\thesection}{Appendix \oldthesection}
  \section{#1}\let\thesection\oldthesection}

\input{appendix-proof}
%\input{appendix-alg}
\input{appendix-maxsat}
\input{appendix-data}

\end{document}
